COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	The following is the file organization in the project:
C00005 00003	the file dependency is as follows:
C00008 ENDMK
C⊗;
;The following is the file organization in the project:
;There may be some changes of disposition w.r.t. the presentation in the paper
;G.Bellin and J.Ketonen, Experiments in Authomatic Theorem Proving
;but the same material covered.

;Here the filename is given:

;normal[ekl,sys]                ;a normalizer of (propositional) expressions

;set[ekl,sys]                   ;rudiments of set theory

;natnum[ekl,sys]                ;facts of natural numbers, involving <,',+ and *

;minus[ekl,sys]                 ;facts of natural numbers, involving ≤ and -

;sums[ekl,sys]                  ;finite sums and unions

;lispax[ekl,sys]                ;axioms of LISP

;length[ekl,sys]                ;length of lists

;nth[ekl,sys]                   ;the nth function and its relatives

;appl[ekl,sys]                  ;two ways of defining finite functions

;mult[ekl,sys]                  ;multiplicity and their properties

;pigeon[ekl,sys]                ;the prigeon hole principle and two applications

;invima[ekl,sys]                ;generalization (third application)

;assoc[ekl,sys]                 ;permutations are a group (using alist)

;permp[ekl,sys]                 ;permutations are a group (lists, using predicates)

;permf[ekl,sys]                 ;permutations are a group (lists, using functions)

;the file dependency is as follows:

;      natnum        normal              lispax
;         |            |                    |
;         |____________|                    |
;               |                           |
;               ↓                           ↓
;             minus                        set 
;               |                           |
;               |___________________________|
;                            |
;                            ↓
;                           sums       
;                            ↓
;                         length
;                            ↓
;                           nth 
;                            ↓
;                           appl
;                            |
;       _____________________|_____________________
;       |           |                 |           |
;       ↓           ↓                 ↓           ↓
;     mult        assoc             permp        perf 
;       ↓
;    pigeon 
;       ↓
;    invima 
 
;facts about reverse are given in the following order

;                lispax
;                   |    
;                   ↓                 
;                reverse           natnum
;                   |                 |
;                   |_________________|
;                            |                                       
;                            ↓
;                          lthrev